Inference at * 
Iof proof for Lemma can-apply-compose-sq:


  A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
  can-apply(f o g  ;x) ~ (can-apply(g;x)  can-apply(f;do-apply(g;x))) 

latex

 by ((UnivCD) 
CollapseTHENA (Auto)) 
CollapseTHEN ((RepUR ``do-apply can-apply p-compose`` ( 0
C)) 
CollapseTHEN (((GenConclAtAddr [1;1;1;1]) 
CollapseTHENA (Auto)) 
CollapseTHEN ((D (-2)
C) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN (Auto))))) 

latex

C.

Definitions

Type, f o g  , can-apply(f;x), do-apply(f;x), f(a), Top, s = t, x:A. B(x), P  Q, x:AB(x), t  T, left + right